$\vdash$  $\forall$$T$:Type. p{-}id() $\in$ $T$$\rightarrow$($T$ + Top)